* Undo workaround with short-circuiting operations (#269)

* redo short-circuiting operations

* Undo change

* Update router/dataplane.go

* increase timeout for epic (#278)

* experiment with disabling NL (#265)

* experiment with disabling NL

* enable the wildcard optimization for when NL is disabled

* Apply suggestions from code review

* Drop unnecessary annotations in `Run` (#279)

* drop unnecessary annotations

* fix precond error

* fix verification error

* cleanup

* fix tiny error

* bring changes to the io spec to speed things a little (#281)

* Add config for overflow in the CI (#247)

* start overflow checking

* backup

* fix flags

* Apply suggestions from code review

* disable checks in all packages for now

* Update .github/workflows/gobra.yml

* Reduce permission amount to buffer for decodeFromLayers (#285)

* R40

* epic

* extn

* onehop

* reduce permission amount of decode layers

* cosmetic changes (#286)

* Fix warning in the CI (#288)

* Update gobra.yml to disableNL (#289)

* simplify Decoded.Reverse (#295)

* Cherry-pick #4483 from `scionproto/scion` (#292)

* cherry-pick 4483

* undo change to test due to the use of (yet) undefined symbols

* fix verification error

---------

Co-authored-by: jiceatscion <139873336+jiceatscion@users.noreply.github.com>

* change permissions amount for decode SCMPTraceRoute (#299)

* First batch of changes from PR #248 (#306)

* first batch of changes from the IO spec

* Apply suggestions from code review

* adapt config options

* Add checks for termination modulo blocking (#309)

* add termination checking if we ignore locking

* add termination checks modulo locking

* backup

* fix termination measure

* fix verification errors

* fix verification error

* Verify the IO behavior (a.k.a., basis PR) (#248)

* manually trigger workflow

* manually trigger workflow

* raw byte to spec for segments and hopfields

* bugfix

* import fix

* bugfix after gobra update

* spec to pkt (currSeg)

* spec to pkt (left, mid, right)

* spec to pkt (termination)

* code clean up

* clean up

* improvements

* instantiate abstract functions with bodies

* progress io spec

* formatting

* specification fixes

* IO-spec to pkt rewritten

* clean up

* improve readability

* rename of function lengthOfCurrSeg

* extract asid-seqence from raw pkt

* missing trigger

* quick fix

* Update router/dataplane_spec.gobra

Co-authored-by: Dionysios Spiliopoulos <32896454+Dspil@users.noreply.github.com>

* Apply suggestions from code review

Co-authored-by: João Pereira <joaopereira.19@gmail.com>

* readability improvements

* further improvements

* replace 4 by its constant InfoLen

* readability improvement

* constant for metaLen in package path

* Update router/io-spec.gobra

Co-authored-by: João Pereira <joaopereira.19@gmail.com>

* minor improvements

* move validMetaLenInPath() to test file

* io-spec in Run

* add body to absIO_val

* fix merge mistake

* fix merge mistake

* fix typo

* io-spec skeleton for processPkt and processSCION

* import fix

* Update router/io-spec.gobra

* unit

* well formdness

* relate dataplane with dataplaneSpec

* various fixes

* Update verification/io/values.gobra

* permission fix for dpSpecWellConfigured

* permission fix in rc

* fix verification error

* dp.Valid() as opaque

* backup

* format spacing

* improve perf; drop assumption

* fix formatting

* Update router/dataplane.go

* formatting postconditions of processPkt, processSCION

* fix extra permission

* typo

* processSCION had the same issue

* ingressID is preseved intead of sInit

* Revert "ingressID is preseved intead of sInit"

This reverts commit 88db3fd.

* Revert "processSCION had the same issue"

This reverts commit 71aadfe.

* Updated IO-Spec-Function to Correlate Bytes with Terms (#262)

* fixes in the asid extraction functions

* pre-/postconditions for process

* fix formatting

* fix same issue in processSCION

* fix var names

* precondition changes in hopfield and asidFromIfs

* prostcondition fix in process and processSCION

* update imports links

* Apply suggestions from code review

---------

Co-authored-by: Dspil <dennisspiliopoylos@gmail.com>
Co-authored-by: João Pereira <joaopereira.19@gmail.com>

* made absIO_val opaque

* use artificial triggers for quantifiers inside IO resources (#280)

* AbsPkt improvements (#270)

* absPkt opaque and other improvements

* quick fixes

* changed permission from R55 to R56

* added missing permission amount in ReadBatch

* fixed pre/postconditions of processPkt, processSCION and process

* fixed opaque format

---------

Co-authored-by: João Pereira <joaopereira.19@gmail.com>

* Verify send guard in Run (#263)

* remove send operation

* lemma for smaller buffer result in same abstract pkt

* progress send guard

* progress send guard

* Fix incompleteness and continue with send guard (#273)

* backup

* backup

* backup

* backup

* backup

* drop space

* pick better triggers

* add necessary lemma and call to it; contains an assume false that needs to be dropped

* backup

* backup

* add missing loop invariant about ingressID

* backup

* backup

* fix verification error

* try out a simpler trigger

* widen lemma for absIO_val (#268)

* widen lemma for abspkt (non termianting)

* abspkt proven

* renamed io-spec-lemmas

* io val also proven

* cleanup

* merged markus' abspkt improvements

* consdir lemma

* proved

* reinstate lemma4

* fix verification error

* Simplify widen lemma from #268 (#282)

* start simplifying

* continue simplifying

* continue simplifying stuff

* continue simplifying

* continue simplifying

* simplify further

* finish for now

* Update router/io-spec.gobra

---------

Co-authored-by: João Pereira <joaopereira.19@gmail.com>

* Continue send (#283)

* widen lemma for abspkt (non termianting)

* abspkt proven

* renamed io-spec-lemmas

* io val also proven

* cleanup

* merged markus' abspkt improvements

* consdir lemma

* proved

* reinstate lemma4

* fix verification error

* Simplify widen lemma from #268 (#282)

* start simplifying

* continue simplifying

* continue simplifying stuff

* continue simplifying

* continue simplifying

* simplify further

* finish for now

* Update router/io-spec.gobra

* finish send in Run

* propagate changes to processSCION

---------

Co-authored-by: Dspil <dennisspiliopoylos@gmail.com>

* backup

* adapt to the new syntax of backend annotations

* clean-up

* changes according to feedback

---------

Co-authored-by: João Pereira <joaopereira.19@gmail.com>
Co-authored-by: Dionysios Spiliopoulos <32896454+Dspil@users.noreply.github.com>
Co-authored-by: Dspil <dennisspiliopoylos@gmail.com>

* IO specification skeleton in process (#284)

* absPkt opaque and other improvements

* tests for local enter guard

* new approach for absPkt

* tests with GetIngressIDNotZero()

* fix verification error

* progress io-skeleton in process

* progress Xover

* progress io-spec skeleton in process

* removed dulicate of lemma

* fix verification error

* removed old concurrency test

* refactored absPkt

* continue refactoring of absPkt

* fixed postcondition in process

* progress lemmas for io-spec

* addressed feedback

* progress in updateNonConsDirIngressSegID

* fix verification errors

* Prove IO lemmas in `path/scion` (#290)

* try to prove lemma

* backup

* fix incompletness via additional lemma

* fix verification error

* fix verification errors and clean up

* fix verification errors introduced in the latest changes to the PR

* fix consistency error

* add lemmas for updateNonConsDirIngressSegID()

* Change to EQAbsHeader (#293)

* changed EQAbsHeader

* readbility improvements

* progress in handleRouterAlerts methods

* Fix verification errors in dependencies (#291)

* backup

* backup

* backup

* simplify Decoded.Reverse

* clean-up

* add section header

* drop comment

* fix  verification errors in processEgress and DoXover
addressing feedback
clean up

---------

Co-authored-by: João Pereira <joaopereira.19@gmail.com>

* Add functional spec to `InfoField.SerializeTo` (#300)

* absPkt opaque and other improvements

* tests for local enter guard

* new approach for absPkt

* tests with GetIngressIDNotZero()

* fix verification error

* progress io-skeleton in process

* progress Xover

* progress io-spec skeleton in process

* removed dulicate of lemma

* fix verification error

* removed old concurrency test

* refactored absPkt

* continue refactoring of absPkt

* fixed postcondition in process

* progress lemmas for io-spec

* addressed feedback

* progress in updateNonConsDirIngressSegID

* fix verification errors

* Prove IO lemmas in `path/scion` (#290)

* try to prove lemma

* backup

* fix incompletness via additional lemma

* fix verification error

* fix verification errors and clean up

* fix verification errors introduced in the latest changes to the PR

* fix consistency error

* add lemmas for updateNonConsDirIngressSegID()

* backup

* Change to EQAbsHeader (#293)

* changed EQAbsHeader

* readbility improvements

* backup

* backup

* simplify Decoded.Reverse

* progress in handleRouterAlerts methods

* clean-up

* add section header

* drop comment

* Fix verification errors in dependencies (#291)

* backup

* backup

* backup

* simplify Decoded.Reverse

* clean-up

* add section header

* drop comment

* backup

* backup

* fix  verification errors in processEgress and DoXover
addressing feedback
clean up

* backup

* drop one assume

* readability improvements

* backup

* backup

* simplify proof

* adapt lemmas

* verify spec for SerializeTo of infofield

* Missing Postcondition in Process (#301)

* absPkt opaque and other improvements

* tests for local enter guard

* new approach for absPkt

* tests with GetIngressIDNotZero()

* fix verification error

* progress io-skeleton in process

* progress Xover

* progress io-spec skeleton in process

* removed dulicate of lemma

* fix verification error

* removed old concurrency test

* refactored absPkt

* continue refactoring of absPkt

* fixed postcondition in process

* progress lemmas for io-spec

* addressed feedback

* progress in updateNonConsDirIngressSegID

* fix verification errors

* Prove IO lemmas in `path/scion` (#290)

* try to prove lemma

* backup

* fix incompletness via additional lemma

* fix verification error

* fix verification errors and clean up

* fix verification errors introduced in the latest changes to the PR

* fix consistency error

* add lemmas for updateNonConsDirIngressSegID()

* Change to EQAbsHeader (#293)

* changed EQAbsHeader

* readbility improvements

* Revert "Update gobra.yml to disableNL (#289)"

This reverts commit 1e60830.

* progress in handleRouterAlerts methods

* Fix verification errors in dependencies (#291)

* backup

* backup

* backup

* simplify Decoded.Reverse

* clean-up

* add section header

* drop comment

* fix  verification errors in processEgress and DoXover
addressing feedback
clean up

* fix verification error

* changed postcondition in process

* fix verification error

* fix verification error

* Update gobra.yml

* added postcondition to packSCMP

---------

Co-authored-by: João Pereira <joaopereira.19@gmail.com>

* Drop unnecessary function `hopFieldsNotConsDir` (#303)

* reverse hopFieldsNotConsDir once

* remove hopfieldsNotConsDir

* hopFieldsConsDir => hopFields

---------

Co-authored-by: João Pereira <joaopereira.19@gmail.com>

* Update IO-spec to drop the `xover_core` event (#302)

* progress updating the IO-spec

* finish updating new IO-spec

* Fix precondition of `processSCION` (#307)

* start fixing pres of processSCION

* backup

* backup

* Drop unnecessary assertions

* tiny fmt

* streamline msgterm assumptions (#308)

* improve verification time of processPkt

* IO-spec update for link check logic (#310)

* io-spec update

* proof of link logic

* fix verification errors

* drop assumption in validateSrcDstIA()

* fix verification error

* Update pkg/slayers/path/scion/raw.go

* Pre/Post conditions of processPkt (#312)

* progress with pre and post conditions for io-spec in processPkt

* fix verification error

* changes in process

* additional temporary assumptions in process()

* cleanup

---------

Co-authored-by: João Pereira <joaopereira.19@gmail.com>

* fmt

---------

Co-authored-by: MLETHZ <mlimbeck@student.ethz.ch>
Co-authored-by: Markus Limbeck <92801626+mlimbeck@users.noreply.github.com>
Co-authored-by: João Pereira <joaopereira.19@gmail.com>

* Update names of functions according to the changes in the IO-spec (#314)

* minor renaming and merging of functions

* further renaming

* Cleanup unnecessary code in the stdlib formalization (#315)

* cleanup unnecessary code in the stdlib formalization

* replace occurrences of names with 'VerifiedSCION'

* backup (#324)

* Remove more names (#325)

* backup

* remove more

* Disable conditionalizePermissions (#319)

* Update gobra.yml

* Update gobra.yml

* fix verification error

* fixed precondition of XoverEvent

* enable moreJoins impure (#321)

* invariant strengthening

* undo change to the state consolidator

---------

Co-authored-by: mlimbeck <mlimbeck@student.ethz.ch>
Co-authored-by: Dspil <dennisspiliopoylos@gmail.com>

* Refactored Widen-lemma (#327)

* Update gobra.yml

* Update gobra.yml

* fix verification error

* fixed precondition of XoverEvent

* enable moreJoins impure (#321)

* invariant strengthening

* progress widen-lemma proof

* fix verification error

* proven?

* fix

* bugfix

* Update router/widen-lemma.gobra

Co-authored-by: João Pereira <joaopereira.19@gmail.com>

* Update router/widen-lemma.gobra

Co-authored-by: João Pereira <joaopereira.19@gmail.com>

* joao

* indent

---------

Co-authored-by: João Pereira <joaopereira.19@gmail.com>
Co-authored-by: Dspil <dennisspiliopoylos@gmail.com>
Co-authored-by: Dionysios Spiliopoulos <32896454+Dspil@users.noreply.github.com>

* enable chop 10 in the CI (#328)

* drop assumption in processPkt (#318)

Co-authored-by: João Pereira <joaopereira.19@gmail.com>

* fix termination measuer (#329)

* change triggers in absPktWidenLemma (#330)

* change triggers in abspktwidenlemma

* triggers

* remove quantifiers

* Drop Assumption in validateEgressID (#326)

* Update gobra.yml

* Update gobra.yml

* fix verification error

* fixed precondition of XoverEvent

* enable moreJoins impure (#321)

* drop assumption in validateEgressID and process

* clean up

* invariant strengthening

* undo change to the state consolidator

* refactored wellConfigured assumptions

* finish proof of EgressIDNotZeroLemma

* Apply suggestions from code review

* removed TopologySpec

* minor fmt

* fix verification error

* removed comments

Co-authored-by: João Pereira <joaopereira.19@gmail.com>

---------

Co-authored-by: João Pereira <joaopereira.19@gmail.com>
Co-authored-by: Dspil <dennisspiliopoylos@gmail.com>
Co-authored-by: Dionysios Spiliopoulos <32896454+Dspil@users.noreply.github.com>

* router: forbid bouncing packets internally (#4502) (#332)

Brings changes from scion pr 4502

Co-authored-by: Matthias Frei <matzf@scion.org>

* Proof of Internal Packet Bouncing fix (#4502) (#333)

* proof of scionfix #4502

* feedback

* drop assume in processOHP()

* change getDomExternal()   to opaque

* fix comment

* verification fix and simplification

* fix verification errors

* feedback

* bring changes from #243 (#335)

* Drop `trusted` annotation in method (#339)

* drop trusted from method

* IO-spec lemmas (#334)

* progress open io-lemmas

* fix verification errors

* refactoring

* fix verification error

* Enable `conditionalizePermissions` for the `router` (#340)

Marco observed that a long time is spent on (sequential) pure function verification in the router package. He also suggested that using `conditionalizePermissions` might reduce the number of branches in these functions (`moreJoins 1` does not have any effect on pure functions), which might speed up verification.

* Refactoring of absPkt (#341)

* drop DataPlaneSpec param from absPkt

* headerOffset change in absPkt

* fix syntax error

* fix verification errors

* fix verification errors

* fix LastHopLemma

* Proof of incPath (#344)

* progress incPath proof

* Apply suggestions from code review

Co-authored-by: João Pereira <joaopereira.19@gmail.com>

* fmt of widen-lemma

* further fmt

* feedback

* add comment

* Update router/dataplane.go

* Apply suggestions from code review

---------

Co-authored-by: João Pereira <joaopereira.19@gmail.com>

* simplify path/scion (#346)

* Verify assumptions in SCION.DecodeFromBytes (#345)

* progress scion- decodeFromBytes

* revert change of call s.Path.DecodeFromBytes()

* fix verification error

* fix permission in rawPath

* establish validPktHeader in parsePath

* fix verification errors

* fixed permission and refactored EqAbsHeader

* fixed syntax errors

* fix verification error

* fix permission

* introduces additional spec to the Path interface

* remove unnecessary preconditions

* proof of parse path assumption

* simplification in epic.DecodeFromBytes

* feedback

* Update pkg/slayers/path/scion/raw.go

Co-authored-by: João Pereira <joaopereira.19@gmail.com>

* add quantifier to GetCurrentHopField() and GetCurrentInfoField() to avoid code changes

* Apply suggestions from code review

Co-authored-by: João Pereira <joaopereira.19@gmail.com>

* formatting

* simplify onehop

* improve io_msgterm_spec.gobra

---------

Co-authored-by: João Pereira <joaopereira.19@gmail.com>

* Drop assumption in parsePath (#348)

* drop assumption in parsePath

* Update router/dataplane.go

Co-authored-by: João Pereira <joaopereira.19@gmail.com>

* rename arrayCongruence()  to AbsMacArrayCongruence()

---------

Co-authored-by: João Pereira <joaopereira.19@gmail.com>

* Use Gobra's built-in ghost fields (#337)

* add ghost fields

* fix type errors so far

* backup

* clean-up

* convert more adt types to structs

* make read not trusted

* Update router/dataplane_concurrency_model.gobra

* cleanup

* change equality

* rever changes to ===

* clean-up

* Fix ghostness of output params (#349)

* fix ghostness of a few outparams

* backup

* fix fmt (#351)

* big clean-up (#354)

* Drop Assumption in SetInfoField (#350)

* proof setInfoField

* fix verification errors

* fix syntax error

* fix verification errors

* formatting

* simplification attempt

* Apply suggestions from code review

Co-authored-by: João Pereira <joaopereira.19@gmail.com>

* refactoring

* fix verification error

* fixed LeftSegEquality()

* formatting

* Apply suggestions from code review

Co-authored-by: João Pereira <joaopereira.19@gmail.com>

* feedback

* renaming AbsSlice_Bytes to Bytes

* adding documentation

---------

Co-authored-by: João Pereira <joaopereira.19@gmail.com>

* small clean-up (#355)

* Simplification of segLens (#356)

* simplification of SegLens

* remove preconditions on CombineSegLens

* fix verification error

* renaming

* make Len impure and add LenSpec (#357)

* Format `info_hop_setter_lemmas.gobra` (#359)

* fmt

* fmt

* Simplify validity criteria of paths (#352)

* backup

* backup

* continue refactor

* backup

* Update pkg/slayers/path/epic/epic_spec_test.gobra

* backup

* merge with master

* backup

* fix verification error

* backup

* simplify preconditions

* drop unnecessary method

* fix annotation

* fix verification error

* minor fixes in styling

* fix verification errors

* proof of IsSupportedPkt (#363)

* Drop two assumptions and merge validity criteria `StronglyValid` and `FullyValid` (#366)

* backup

* backup

* fix verification error

* fix test

* fix another verification error

* fix verification error

* drop StronglyValid criteria

* cleanup

* Update gobra.yml

* Update .github/workflows/gobra.yml

* Update .github/workflows/gobra.yml

* Drop SetHopfield related assumptions (#368)

* proof of sethopfield and io-assumptions

* fix syntax errors

* fix termination measure

* fix verification errors

* simplifications and comments

* fix syntax error

* feedback

* fix verification error

* renaming

* space between arithmetic operands

* increase timeout of path/scion

* fix verification error

* test: parallelizeBranches for dependencies

* test: increase timeout for scion package to 20 min

* test: increase timeout for scion package to 1h

* use parallelizeBranches only for scion package

* stronger precondition for setHopfield

* Revert "stronger precondition for setHopfield"

* test: scion pkg without parallelizeBranches

* Revert "test: scion pkg without parallelizeBranches"

* fix merging mistake

* assume postconditions in setHopfield

* add comment to IO assumptions

* increase timeout for scion package

* revert timeout increase

* feedback

* Drop IO-assumptions in processOHP (#369)

* move assumption from processOHP to updateSCIONLayer

* proof of assumptions in processOHP

* test: moreJoins for SerializeTo in slayers

* fix verification error

* feedback

* add moreJoins to SerializeTo()

* fix sytnax errors

* fix some verification errors

* make `hf_valid` opaque (#372)

* make hf_valid opaque

* backup

* backup

* might have to reverse this

* backup

* backup

* Update router/io-spec-abstract-transitions.gobra

* Update README.md

* progress with verification errors

---------

Co-authored-by: João Pereira <joaopereira.19@gmail.com>
Co-authored-by: Dionysios Spiliopoulos <32896454+Dspil@users.noreply.github.com>
Co-authored-by: jiceatscion <139873336+jiceatscion@users.noreply.github.com>
Co-authored-by: Dspil <dennisspiliopoylos@gmail.com>
Co-authored-by: Matthias Frei <matzf@scion.org>